Uma Lógica para a Referência Ambígua by Andressa Sebben
Master's Thesis in Computer Science
Department of Informatics and Statistics
Federal University of Santa Catarina - Florianópolis/SC - Brazil
2007, 203 pages
Abstract: Description operators make terms from variables and formulas of logical systems. Several
theories introduce description operators to represent, in formal languages, the definite
article (the) and the indefinite article (a/an) of natural languages. However, the known approaches
do not offer a treatment for ambiguous terms. The logic LAR (Logic of Ambiguous
Reference), firstly presented in Buchsbaum (2002), was proposed to represent suitably these
situations, which appear very often in mathematics and in everyday speech. LAR presents a
different way to treat descriptions, through the association of each term to a collection of objects
of the universe of discourse, in opposition to usual semantics, which associate each term
to a single object. Thus, we can deal uniformly with univocal, vacuous and ambiguous descriptions.
Another remarkable feature of LAR is the concept of comprising, which behaves as
an unidirectional equality. These two features, description and comprising, allow a knowledge
representation closer to usual linguistic practice. This work presents LAR in detail, including
the proof of original results and some corrections, besides a presentation of many examples. Finally,
a comparison between LAR and the description logics of Bertrand Russell, John Barkley
Rosser and David Hilbert is accomplished.
Uma Proposta de Aprendizado
da Lógica utilizando um Ambiente Virtual de Aprendizagem Colaborativa, by Fernando Cezar Vieira Malange
Master's Thesis in Computer Science
Department of Informatics and Statistics
Federal University of Santa Catarina - Florianópolis/SC - Brazil
2005, 108 pages
Abstract: In this study a basic course on Logic was
developed, using technologies developed for the Internet in relation to
distance education activities. It aims to apply the socio-cultural approach
to the obtention of a basic knowledge of logic, with the use of a computational
system through a virtual environment of cooperative learning. It presents
an introduction to the most basic aspects of General Logic, through appropriate
tools for distance-learning. It addresses the traditional concepts of Classic
Logic and some of Non-Classic Logic as motivation for later studies, as
such logics have found application in several areas of knowledge, mainly
in the technological applications of artificial intelligence, philosophy,
robotics, electric engineering and the fundamentals of mathematics. Currently,
several computational systems have been proposed to give support to the
educative process using the Internet as a form of media interacting between
the two sides of the educative process. Such systems, known as AVAC (Ambientes
Virtuais de Aprendizagem Colaborativa – Virtual Environment for Collaborative
Learning), provide interaction, but by themselves, they do not guarantee
full interaction between the players in the educative process. Based on
a theoretical foundation and on diverse analyses of AVACs, the use of Claroline
was selected which offersa group of resources and technologies capable of
obtaining good levels of interaction and learning, along with the possibility
for the insertion of other educational tools, thus constituting a fully
efficient environment for the support of logic education activities based
on cooperation. The pedagogical project, to which most effort was directed
during the development of the course, takes into account the main pedagogical
presuppositions relating to cooperative and constructivist learning and
to distance learning. With the use of tools specific to logic, the course
consists of a virtual learning environment capable of supporting educational
activities based on cooperation.
Um Método dos Tablôs
por Prova Direta para a Lógica Clássica, by Maurício Correia Lemes Neto
Master's Thesis in Computer Science
Department of Informatics and Statistics
Federal University of Santa Catarina - Florianópolis/SC - Brazil
2004, 80 pages
Abstract: This work develops proof trees by tableaux
in a different way. It is named direct method, because the possible conclusion
is placed in the initial tableau, without negating it. Instead it, the refutation
method uses the negation of the possible conclusion. In a tableau system
by direct proof for classical logic, each branch is semantically connected
to the disjunction of its formulas, and the complete tableau corresponds
to the conjunction of all these disjunctions. In each of these methods for
classical logic, the direct or the indirect one, a branch is closed if it
contains two contradictory formulas. In the indirect method, the closure
of all branches implies the unsatisfiability of the negation of possible
conclusion, which implies its validity.
Dedução Automática por
Tableaux Estruturada em XML, by Parcilene Fernandes de Brito
Master's Thesis in Computer Science
Department of Informatics and Statistics
Federal University of Santa Catarina - Florianópolis/SC - Brazil
2003, 108 pages
Abstract: This thesis main goal is to describe the development of a theorem
prover according to the Tableau Method. To achieve this, two refinements
are proposed to make the method more efficient concerning to the proof steps.
These refinements are related to the formulas sorting and to variable instantiation,
aiming to decrease the number of elements inserted into the tree and to
increase the efficiency regarding to the number of nodes. The Java language
was used to implement the prover, allowing the manipulation of formulas
specified as XML documents. In the end of this work, the theorem prover
efficiency is verified against others provers, comparing the systematization
of proof steps and the results achieved.
Refinamentos para o Método dos Tableaux by Leticia Carvalho Pivetta Fendt
Master's Thesis in Computer Science
Department of Informatics and Statistics
Federal University of Santa Catarina - Florianópolis/SC - Brazil 2000, 167 pages
Abstract: Some enhancements over traditional
tableau method are proposed, aiming to diminish the number of nodes of proof
trees, and to increase the probability of acquiring answers. Three distinct
algorithms are specified and implemented, based on the traditional tableau
method for classical logic. The most sophisticated of them applies the unification
procedure, used by resolution method. A series of tests is done, for verifying
the attainment of the initial objectives.
Uma Lógica para a Referência Ambígua defendida por Andressa Sebben
Dissertação de Mestrado em Ciência da Computação
Departamento de Informática e de Estatística
Universidade Federal de Santa Catarina, Florianópolis/SC
2007, 203 páginas
Resumo: Descritores são operadores que formam termos a partir de variáveis e fórmulas de sistemas
lógicos. Diversas teorias introduzem descritores para representar, em linguagens formais,
o artigo definido (o/a) e o artigo indefinido (um/uma) das linguagens naturais. Entretanto, as
abordagens mais conhecidas não oferecem um tratamento para termos ambíguos. A lógica
LAR (Logic of Ambiguous Reference), originalmente apresentada em Buchsbaum (2002), foi
proposta para representar adequadamente estas situações, bastante comuns na matemática e na
linguagem cotidiana. LAR apresenta um modo diferenciado de tratar descrições, através da
associação de cada termo a uma coleção de objetos do universo de discurso, em oposição às
semânticas usuais, as quais associam cada termo a um único objeto. Dessa forma, pode-se tratar
uniformemente descrições unívocas, vácuas e ambíguas. Outra característica de destaque é
o conceito de abrangência, o qual opera como uma igualdade unidirecional. Essas duas características,
descrição e abrangência, permitem uma representação de conhecimento mais próxima
da prática linguística usual. Este trabalho apresenta um detalhamento de LAR, incluindo provas
dos resultados originais e algumas correções, além da apresentação de diversos exemplos. Por
fim, LAR é comparada às lógicas descritivas de Bertrand Russell, John Barkley Rosser e David
Hilbert.
Uma Proposta de Aprendizado
da Lógica utilizando um Ambiente Virtual de Aprendizagem Colaborativa, defendida por Fernando Cezar Vieira Malange
Dissertação de Mestrado em Ciência da Computação
Departamento de Informática e de Estatística
Universidade Federal de Santa Catarina, Florianópolis/SC
2005, 108 páginas
Resumo: Este trabalho realiza o desenvolvimento de um
curso básico de Lógica, utilizando tecnologias desenvolvidas para a Internet
em atividades educacionais à distância. É utilizado um sistema computacional
através de um ambiente virtual de aprendizagem cooperativa. Através de ferramentas
apropriadas para o ensino à distância, é apresentada uma iniciação ao lado
mais básico da Lógica Geral, sobre os conceitos primordiais da Lógica Clássica,
e de algumas das Lógicas Não Clássicas, como motivação para estudos posteriores,
já que tais lógicas têm encontrado aplicações em várias áreas do saber,
principalmente em aplicações tecnológicas da inteligência artificial, na
filosofia, na robótica, na engenharia elétrica e nos fundamentos da matemática.
Atualmente, vários sistemas computacionais se propõem a dar suporte ao processo
educativo utilizando a Internet como mídia de interação entre os pares do
processo educativo. Tais sistemas, conhecidos como AVAC (Ambientes Virtuais
de Aprendizagem Colaborativa), proporcionam interação, mas por si sós não
garantem interatividade total entre os atores do processo educativo. Com
base na fundamentação teórica e na análise de diversos AVAC’s, optou-se
pela utilização do Claroline, que conta com um grupo de recursos e tecnologias
capazes de obter bons níveis de interatividade e aprendizagem, além da possibilidade
da inserção de outras ferramentas educacionais, constituindo assim um ambiente
plenamente eficiente no suporte de atividades educacionais da lógica baseadas
na cooperação. O projeto pedagógico, uma das etapas mais trabalhadas no
desenvolvimento do curso, leva em conta os principais pressupostos pedagógicos
da aprendizagem cooperativa, construtivista, e da Educação à Distância.
Com a utilização de ferramentas específicas de lógica, o curso desenvolvido
constitui-se em um ambiente virtual de aprendizagem capaz de suportar atividades
educacionais baseadas na cooperação.
Um Método dos Tablôs
por Prova Direta para a Lógica Clássica, defendida por Maurício Correia Lemes Neto
Dissertação de Mestrado em Ciência da Computação
Departamento de Informática e de Estatística
Universidade Federal de Santa Catarina, Florianópolis/SC
2004, 80 páginas
Resumo: Este trabalho desenvolve uma forma diferente
de se obter árvores de prova por tablôs. Denominamos esse método
de direto, por causa da característica em que a possível conclusão
é inserida no tablô inicial, sem negá-la. Já
o método dos tablôs por refutação se utiliza
da negação da possível conclusão. No sistema
de tablôs por prova direta para a lógica clássica, cada
ramo está relacionado semanticamente à disjunção
das fórmulas que o compõem, e o tablô completo corresponde
semanticamente à conjunção de todas essas disjunções.
Em qualquer um dos métodos baseados em tablôs para a Lógica
Clássica, tanto direto quanto indireto, um ramo é considerado
fechado se o mesmo contiver duas fórmulas contraditórias.
No método direto o fechamento de um ramo corresponde à sua
validade semântica, a qual implica, no caso do fechamento de todos
os ramos, na validade da possível conclusão. Já no
método indireto o fechamento de todos os ramos corresponde à
insatisfatibilidade da negação da possível conclusão,
o que por sua vez implica na validade da mesma.
Dedução Automática por
Tableaux Estruturada em XML, defendida por Parcilene Fernandes de Brito
Dissertação de Mestrado em Ciência da Computação
Departamento de Informática e de Estatística
Universidade Federal de Santa Catarina, Florianópolis/SC
2003, 108 páginas
Resumo: Este trabalho tem como objetivo descrever o
desenvolvimento de um provador de teoremas segundo o Método dos Tableaux.
Para isso, foram propostos dois refinamentos com o intuito de tornar o método
mais eficiente durante as etapas de prova. Esses refinamentos tratam da
ordenação das fórmulas e da instanciação das variáveis, buscando diminuir
a inserção de elementos na árvore, propiciando, assim, uma maior eficiência
em relação ao número de nós. A linguagem Java foi utilizada para a implementação
do provador, possibilitando a manipulação das fórmulas estruturadas como
documentos XML. Ao final do trabalho, é verificada a eficiência do provador
através da comparação com outros provadores em relação à sistematização
das suas etapas de prova e dos resultados obtidos.
Refinamentos para o Método dos Tableaux defendida por Leticia Carvalho Pivetta Fendt
Dissertação de Mestrado em Ciência
da Computação
Departamento de Informática e de Estatística
Universidade Federal de Santa Catarina, Florianópolis/SC 2000, 167 páginas
Resumo: São propostos refinamentos
sobre o método dos tableaux, tal como tradicionalmente apresentado,
visando diminuir o número de nós das árvores de prova,
bem como aumentar a possibilidade de obtenção de respostas.
Para isto especificamos e implementamos três diferentes algoritmos
baseados no método tradicional dos tableaux para a lógica
clássica. O mais sofisticado e avançado dos três métodos
recorre ao procedimento de unificação, comumente utilizado
no método da resolução. Finalizamos este trabalho apresentando
uma série de testes, para verificar experimentalmente a consecução
dos objetivos propostos.
Download
(914 Kbytes)